Nuprl Lemma : decidable__l_member 0,22

A:Type, x:A. (xy:A. Dec(x = y))  (L:A List. Dec((x  L))) 
latex


DefinitionsDec(P), False, x:AB(x), Prop, t  T, (x  l), P  Q, P  Q, P & Q, P  Q, P  Q
Lemmasdecidable wf, cons member, decidable or, decidable functionality, nil member, l member wf, false wf, decidable false

origin